Nuprl Lemma : gcd_p_wf 11,40

a,b,y:. gcd_p(aby prop{1:l} 
latex


DefinitionsP  Q, P  Q, gcd_p(aby), prop{i:l}, t  T, x:AB(x)
Lemmasdivides wf

origin